Nuprl Lemma : ocmon_cancel
13,42
postcript
pdf
g
:OCMon,
u
,
v
,
w
:|
g
|. ((
w
*
u
) = (
w
*
v
)
|
g
|)
(
u
=
v
)
latex
Up
groups
1
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
AntiSym(
T
;
x
,
y
.
R
(
x
;
y
))
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
Connex(
T
;
x
,
y
.
R
(
x
;
y
))
,
Order(
T
;
x
,
y
.
R
(
x
;
y
))
,
monot(
T
;
x
,
y
.
R
(
x
;
y
);
f
)
,
Cancel(
T
;
S
;
op
)
,
Linorder(
T
;
x
,
y
.
R
(
x
;
y
))
,
P
&
Q
Lemmas
ocmon
wf
,
ocmon
properties
origin
g:OCMon, u, v, w:|g|. ((w * u) = (w * v) 
|g|) 
(u = v) g:OCMon, u, v, w:|g|. ((w * u) = (w * v) |g|) (u = v)